es:ES, i:Id, P:({e:E| loc(e) = i} ).
e@i. P(e)  (e@i. (first(e))  P(e) & e@i. ((first(e)))  P(pred(e))  P(e)) 

latex

Definitions	x:A. B(x), , P  Q, x(s), P & Q, P  Q, P  Q, t  T, x. t(x), e@i. P(e), WellFnd{i}(A;x,y.R(x;y)), {T}, Dec(P), P  Q
Lemmas	alle-at wf, es-E wf, Id wf, es-loc wf, assert wf, es-first wf, not wf, event system wf, es-pred wf, es-loc-pred, es-locl-wellfnd, es-locl wf, decidable assert, es-pred-locl